$\forall$$T$:Type, ${\it as}$, ${\it bs}$, ${\it cs}$, ${\it ds}$:$T$ List.
\\[0ex]($\forall$$x$$\in$${\it cs}$. $\neg$($x$ $\in$ ${\it bs}$))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$${\it as}$. $\neg$($x$ $\in$ ${\it ds}$))
\\[0ex]$\Rightarrow$ agree\_on\_common($T$;${\it as}$;${\it cs}$)
\\[0ex]$\Rightarrow$ agree\_on\_common($T$;${\it bs}$;${\it ds}$)
\\[0ex]$\Rightarrow$ agree\_on\_common($T$;${\it as}$ @ ${\it bs}$;${\it cs}$ @ ${\it ds}$)